Report for Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c (Counterexample 141)

Generated on 2025-08-27 13:41:11 by CPAchecker 4.0 / terminationAnalysis

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
typedef enum { false, true } bool;  
2
  
3
extern int __VERIFIER_nondet_int(void);  
4
  
5
int main() {  
6
    int i;  
7
    int up;  
8
    i = __VERIFIER_nondet_int();  
9
    up = 0;  
10
      
11
    while (i > 0) {  
12
        if (i == 1) {  
13
            up = 1;  
14
        }  
15
        if (i == 10) {  
16
            up = 0;  
17
        }  
18
        if (up == 1) {  
19
            i = i+1;  
20
        } else {  
21
            i = i-1;  
22
        }  
23
    }  
24
      
25
    return 0;  
26
}  
DateTimeLevelComponentMessage
2025-08-2713:26:10:820INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2025-08-2713:26:10:905INFOCPAchecker.runCPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started
2025-08-2713:26:10:924INFOCPAchecker.parseParsing CFA from file(s) "Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c"
2025-08-2713:26:11:901INFOCoreComponentsFactory.createAlgorithmUsing Restarting Algorithm
2025-08-2713:26:11:923WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.arg.lateMerge
counterexample.export.exportWitness
2025-08-2713:26:11:924INFOCPAchecker.runAlgorithmStarting analysis ...
2025-08-2713:26:11:931INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ...
2025-08-2713:26:11:976INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
ResourceLimitChecker.fromConfiguration
Using the following resource limits: Thread CPU-time limit of 300s
2025-08-2713:26:12:355INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2713:26:12:670INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPARefiner.<init>
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2713:26:12:680WARNINGCPAs.retrieveCPAOrFailWarning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA)
2025-08-2713:26:12:682INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ...
2025-08-2713:26:12:692INFONestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'.
2025-08-2713:26:12:717WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
FormulaManagerView.<init>
Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2713:26:12:721INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2713:26:12:831INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPARefiner.<init>
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2713:26:12:896WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
FormulaManagerView.<init>
Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2713:26:12:932INFORestartAlgorithm.runStarting analysis 1 ...
2025-08-2713:26:12:933INFOAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.run0
Starting termination algorithm.
2025-08-2713:26:17:236WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:18:693WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:20:373WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:21:957WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:23:698WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:25:628WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:27:110WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:28:811WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:30:002WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:31:640WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:33:472WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:34:712WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:36:430WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:38:276WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:40:086WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:41:304WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:43:832WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:45:357WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:46:675WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:48:379WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:49:678WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:51:328WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:53:021WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:55:743WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:57:129WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:26:58:810WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:02:246WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:03:709WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:06:558WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:08:641WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:10:046WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:11:987WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:13:935WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:16:828WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:18:186WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:20:134WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:23:510WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:25:121WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:27:603WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:30:411WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:32:361WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:35:022WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:37:234WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:40:853WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:42:174WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:44:758WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:48:437WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:50:060WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:53:075WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:54:824WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:57:949WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:27:59:661WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:01:745WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:03:367WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:06:977WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:08:890WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:10:533WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:13:034WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:14:637WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:19:597WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:21:672WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:23:502WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:25:588WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:27:248WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:28:953WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2713:28:29:593INFOAnalysis /cpachecker/config/components/termination-recursion.properties
CounterexampleCheckAlgorithm.checkCounterexample
Error path found, starting counterexample check with CPACHECKER.
2025-08-2713:28:30:047WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
CounterexampleCheck
AutomatonGraphmlParser.getSpecAsProperties
Cannot map specification TRUE to property type. Will ignore it (would only be problematic if this were the termination property).
2025-08-2713:28:30:081WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
CounterexampleCheck
AutomatonGraphmlParser.collectEdgeData
Source A17144 of transition [edge: null] is a violation state. No outgoing edges expected.
2025-08-2713:28:30:136INFOAnalysis /cpachecker/config/components/termination-recursion.properties
CounterexampleCheck
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-08-2713:41:09:404WARNINGShutdownNotifier.shutdownIfNecessaryWarning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.)
2025-08-2713:41:09:406WARNINGForceTerminationOnShutdown$1.shutdownRequestedShutdown requested (The JVM is shutting down, probably because Ctrl+C was pressed.), waiting for termination.
Statistics NameStatistics ValueAdditional Value
Restart Algorithm statistics
Number of algorithms provided 2
Number of algorithms used 1
Last algorithm used /cpachecker/config/components/combinations-parallel-termination.properties
Total time for algorithm 1 897.471s
PredicateCPA statistics
Number of abstractions 728 5% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 397 55%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 331 45%
Times precision was empty 11 2%
Times precision was {false} 328 45%
Times result was cached 1 0%
Times cartesian abs was used 0 0%
Times boolean abs was used 388 53%
Times result was 'false' 249 34%
Number of strengthen sat checks 0
Number of coverage checks 182099
BDD entailment checks 11846
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 13
Avg ABE block size 6.39 sum: 4650, count: 728, min: 0, max: 13
Number of predicates discovered 93
Number of abstraction locations 2
Max number of predicates per location 93
Avg number of predicates per location 47
Total predicates per abstraction 26260
Max number of predicates per abstraction 93
Avg number of predicates per abstraction 36.68
Number of irrelevant predicates 805 3%
Number of preds handled by boolean abs 25451 97%
Total number of models for allsat 27593
Max number of models for allsat 1275
Avg number of models for allsat 71.12
Time for post operator 1.229s
Time for path formula creation 1.214s
Time for strengthen operator 0.258s
Time for prec operator 21.150s
Time for abstraction 21.019s Max: 1.001s, Count: 728
Boolean abstraction 16.907s
Solving time 2.110s Max: 0.013s
Model enumeration time 15.098s
Time for BDD construction 4.118s Max: 0.038s
Time for merge operator 0.071s
Time for coverage checks 0.119s
Time for BDD entailment checks 0.101s
Total time for SMT solver (w/o itp) 17.208s
Number of path formula cache hits 9652 48%
Inside post operator
Inside path formula creation
Time for path formula computation 1.179s
Total number of created targets for pointer analysis 0
Number of BDD nodes 205476
Size of BDD node table 466043
Size of BDD cache 46619
Size of BDD node cleanup queue 2.16 sum: 262783, count: 121752, min: 0, max: 16573
Time for BDD node cleanup 0.036s
Time for BDD garbage collection 0.172s in 52 runs
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
AutomatonAnalysis (NonTerminationLabelAutomaton) statistics
Number of states 1
Total time for successor computation 0.172s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 13966, count: 13966, min: 1, max: 1 [1 x 13966]
Number of states with assumption transitions 0
AutomatonAnalysis (TerminatingFunctions) statistics
Number of states 1
Total time for successor computation 0.019s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 13966, count: 13966, min: 1, max: 1 [1 x 13966]
Number of states with assumption transitions 0
Termination Algorithm statistics
Total time 136.637s
Time for recursion analysis 0.000s
Number of analysed loops 1 100%
Total time for loop analysis 136.630s
Avg time per loop analysis 136.630s
Max time per loop analysis 136.630s
Number of safety analysis runs 70
Avg safety analysis run per loop 70.00
Max safety analysis run per loop 70 for loops [N7]
Total time for safety analysis 28.061s
Avg time per safety analysis run 0.400s
Max time per safety analysis run 1.464s
Number of analysed lassos 71
Avg number of lassos per loop 71.00
Max number of lassos per loop 71 for loops [N7]
Avg number of lassos per iteration 1.01
Max number of lassos per iteration 2
Total time for lassos analysis 108.385s
Avg time per iteration 1.548s
Max time per iteration 4.561s
Time for lassos construction 4.519s
Avg time for lasso construction per iteration 0.064s
Max time for lasso construction per iteration 0.358s
Time for stem and loop construction 0.279s
Avg time for stem and loop construction per iteration 0.003s
Max time for stem and loop construction per iteration 0.030s
Time for lassos creation 4.237s
Avg time for lassos creation per iteration 0.060s
Max time for lassos creation per iteration 0.357s
Total time for non-termination analysis 9.402s
Avg time for non-termination analysis per lasso 0.132s
Max time for non-termination analysis per lasso 0.173s
Total time for termination analysis 94.463s
Avg time for termination analysis per lasso 1.349s
Max time for termination analysis per lasso 4.330s
Total number of termination arguments 5
Avg termination arguments per loop 5.00
Max termination arguments per loop 5 for loops [N7]
affine 5
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 0 0%
Time for counterexample checks 759.813s
Termination Algorithm statistics
Total time 136.637s
Time for recursion analysis 0.000s
Number of analysed loops 1 100%
Total time for loop analysis 136.630s
Avg time per loop analysis 136.630s
Max time per loop analysis 136.630s
Number of safety analysis runs 70
Avg safety analysis run per loop 70.00
Max safety analysis run per loop 70 for loops [N7]
Total time for safety analysis 28.061s
Avg time per safety analysis run 0.400s
Max time per safety analysis run 1.464s
Number of analysed lassos 71
Avg number of lassos per loop 71.00
Max number of lassos per loop 71 for loops [N7]
Avg number of lassos per iteration 1.01
Max number of lassos per iteration 2
Total time for lassos analysis 108.385s
Avg time per iteration 1.548s
Max time per iteration 4.561s
Time for lassos construction 4.519s
Avg time for lasso construction per iteration 0.064s
Max time for lasso construction per iteration 0.358s
Time for stem and loop construction 0.279s
Avg time for stem and loop construction per iteration 0.003s
Max time for stem and loop construction per iteration 0.030s
Time for lassos creation 4.237s
Avg time for lassos creation per iteration 0.060s
Max time for lassos creation per iteration 0.357s
Total time for non-termination analysis 9.402s
Avg time for non-termination analysis per lasso 0.132s
Max time for non-termination analysis per lasso 0.173s
Total time for termination analysis 94.463s
Avg time for termination analysis per lasso 1.349s
Max time for termination analysis per lasso 4.330s
Total number of termination arguments 5
Avg termination arguments per loop 5.00
Max termination arguments per loop 5 for loops [N7]
affine 5
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 0 0%
Time for counterexample checks 759.813s
Code Coverage
Function coverage 1.000
Visited lines 14
Total lines 14
Line coverage 1.000
Visited conditions 8
Total conditions 8
Condition coverage 1.000
CPAchecker general statistics
Number of program locations 26
Number of CFA edges (per node) 29 count: 26, min: 0, max: 2, avg: 1.12
Number of relevant variables 2
Number of functions 1
Number of loops (and loop nodes) 1 sum: 13, min: 13, max: 13, avg: 13.00
Size of reached set 1812
Number of reached locations 18 69%
Avg states per location 100
Max states per location 146 at node N8
Number of reached functions 1 100%
Number of partitions 18
Avg size of partitions 100
Max size of partitions 146 with key N8
Number of target states 1
Size of final wait list 10
Time for analysis setup 0.999s
Time for loading CPAs 0.016s
Time for loading parser 0.227s
Time for CFA construction 0.707s
Time for parsing file(s) 0.256s
Time for AST to CFA 0.172s
Time for CFA sanity check 0.019s
Time for post-processing 0.121s
Time for loop structure 0.005s
Time for AST structure 0.000s
Time for CFA export 0.429s
Time for function pointers resolving 0.003s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.076s
Time for collecting variables 0.049s
Time for solving dependencies 0.003s
Time for building hierarchy 0.000s
Time for building classification 0.020s
Time for exporting data 0.003s
Time for Analysis 897.472s
CPU time for analysis 850.940s
Total time for CPAchecker 898.481s
Total CPU time for CPAchecker 852.620s
Time for statistics 0.672s
Time for Garbage Collector 3.269s in 1952 runs
Garbage Collector(s) used PS MarkSweep, PS Scavenge
Used heap memory 372MB ( 355 MiB) max; 272MB ( 260 MiB) avg; 444MB ( 423 MiB) peak
Used non-heap memory 73MB ( 70 MiB) max; 70MB ( 66 MiB) avg; 74MB ( 70 MiB) peak
Used in PS Old Gen pool 341MB ( 325 MiB) max; 255MB ( 243 MiB) avg; 352MB ( 336 MiB) peak
Allocated heap memory 821MB ( 783 MiB) max; 692MB ( 660 MiB) avg
Allocated non-heap memory 75MB ( 71 MiB) max; 73MB ( 70 MiB) avg
Total process virtual memory 16365MB ( 15607 MiB) max; 16273MB ( 15519 MiB) avg
#Configuration NameConfiguration Value
1analysis.algorithm.termination true
2analysis.machineModel Linux64
3analysis.name terminationAnalysis
4analysis.programNames Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c
5analysis.restartAfterUnknown true
6counterexample.export.exportWitness false
7cpa.arg.lateMerge prevent
8language C
9log.level INFO
10parser.usePreprocessor true
11restartAlgorithm.configFiles components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive
12specification
13statistics.print true
14termination.config terminationAnalysis.properties

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}